sms.3-true.jani:model: info: sms.3-true.jani is an MA model and will be simulated as an MA.
sms.3-true.jani: info: Using default value of 0.95 for the confidence parameter.
sms.3-true.jani:properties[1]: warning: Cycle detection is not available for long-run average properties.
sms.3-true.jani: warning: Using the Chow-Robbins method for relative-width sequential confidence intervals, which guarantees the requested confidence only asymptotically for decreasing width.
Peak memory usage: 66 MB
Analysis results for sms.3-true.jani
Status: Finished
Simulation time: 599.4 s
+ Property Property "Unavailability"
Estimated max. value: 1
Max. confidence interval: [1, 1]
Runs used (best scheduler): 50
Total runs used: 1014050
Schedulers sampled: 1000
Best scheduler: 1084106047
Run type: MA
Status: Finished
+ Max. sample data
Mean: 1
+ Error bounds
Scheduler sampling: The result is a lower bound for the true max. value.
Statement: CI: 100(1 - α)% of intervals contain true value (CLT assumption)
α: 0.050000000000000044